;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Istockretrieval
  (sig get-stocks-in-range (tree start end))
  (sig get-stocks-in-range-by-ticker (tree start end ticker))
  (sig get-stocks-in-range-by-tickers (tree start end tickers))
  (sig get-first-in-range (tree start end ticker))
  (sig get-last-in-range (tree start end ticker))
  (sig get-all-tickers (stocks))
  (sig get-all-tickers-helper (stocks))
  
  (con get-stocks-in-range-returns-list
       (implies (and (and (tree? tree) (natp start)) (natp end)))
       (listp (get-stocks-in-range tree start end)))
  
  (con get-stocks-in-range-by-ticker-returns-list
       (implies (and (and (and (tree? tree) (natp start)) (natp end))) (stringp ticker))
       (listp (get-stocks-in-range-by-ticker tree start end ticker)))
  
  (con get-first-in-range-returns-list
       (implies (and (and (and (tree? tree) (natp start)) (natp end))) (stringp ticker))
       (listp (get-first-in-range tree start end ticker)))
  
  (con get-last-in-range-returns-list
       (implies (and (and (and (tree? tree) (natp start)) (natp end))) (stringp ticker))
       (listp (get-last-in-range tree start end ticker))))